<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<!-- NewPage -->
<html lang="en">
<head>
<title>VarHyp</title>
<link rel="stylesheet" type="text/css" href="../../stylesheet.css" title="Style">
</head>
<body>
<script type="text/javascript"><!--
    if (location.href.indexOf('is-external=true') == -1) {
        parent.document.title="VarHyp";
    }
//-->
</script>
<noscript>
<div>JavaScript is disabled on your browser.</div>
</noscript>
<!-- ========= START OF TOP NAVBAR ======= -->
<div class="topNav"><a name="navbar_top">
<!--   -->
</a><a href="#skip-navbar_top" title="Skip navigation links"></a><a name="navbar_top_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/Var.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/VarHypFormula.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/VarHyp.html" target="_top">Frames</a></li>
<li><a href="VarHyp.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_top">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_top");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_top">
<!--   -->
</a></div>
<!-- ========= END OF TOP NAVBAR ========= -->
<!-- ======== START OF CLASS DATA ======== -->
<div class="header">
<div class="subTitle">mmj.lang</div>
<h2 title="Class VarHyp" class="title">Class VarHyp</h2>
</div>
<div class="contentContainer">
<ul class="inheritance">
<li>java.lang.Object</li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/MObj.html" title="class in mmj.lang">mmj.lang.MObj</a></li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">mmj.lang.Stmt</a></li>
<li>
<ul class="inheritance">
<li><a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">mmj.lang.Hyp</a></li>
<li>
<ul class="inheritance">
<li>mmj.lang.VarHyp</li>
</ul>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</li>
</ul>
<div class="description">
<ul class="blockList">
<li class="blockList">
<dl>
<dt>Direct Known Subclasses:</dt>
<dd><a href="../../mmj/lang/WorkVarHyp.html" title="class in mmj.lang">WorkVarHyp</a></dd>
</dl>
<hr>
<br>
<pre>public class <span class="strong">VarHyp</span>
extends <a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a></pre>
<div class="block">VarHyp -- Variable Hypothesis -- corresponds to the Metamath "$f" statement,
 or "floating hypothesis" statement.
 <p>
 The VarHyp is truly a hypothesis (Hyp) in Metamath, and it is also a
 statement (Stmt), complete with its own label and Formula.
 <p>
 The Formula of a VarHyp consists of a Cnst followed by a Var. For example,
 "wph $f wff ph $." is the famous Metamath declaration of phi, stating that
 variable "ph" <b>is a</b> wff.
 <p>
 <b>On a Tangent Concerning Type Codes and Conversions</b>
 <p>
 By the way, Metamath's base language is strongly typed. Every statement must
 have a Type Code (every Formula is at least one Sym long and the first Sym
 must be a Cnst.) In addition, subsitution of an expression for a variable is
 permitted in Proof Verification (or parsing) only if the two statements have
 the same Type Code.
 <p>
 Apparently a less strict regime was overthrown after an inconsistency was
 "proved". The people of Metamathland quickly discovered the lie and revised
 their system to require their laws and terminology to be well-defined and
 impartially judged by incorruptible automatons.
 <p>
 Fortunately for the expressiveness of Metamath, Type Conversions can be
 defined. The most famous example is Syntax Axiom "cv" in set.mm:
 <p>
 <code></b>
 $( All sets are classes (but not vice-versa!). $)<br>
 cv $a class x $.
 </b></code></div>
<dl><dt><span class="strong">See Also:</span></dt><dd><a href="../../MetamathERNotes.html"> Nomenclature and
      Entity-Relationship Notes</a></dd></dl>
</li>
</ul>
</div>
<div class="summary">
<ul class="blockList">
<li class="blockList">
<!-- =========== FIELD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_summary">
<!--   -->
</a>
<h3>Field Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Field Summary table, listing fields, and an explanation">
<caption><span>Fields</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Field and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#paSubst">paSubst</a></strong></code>
<div class="block">paSubst is used in Proof Assistant unification and holds the root node of
 a subtree which is the assigned substitution value for the VarHyp in a
 single ProofStep.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.Hyp">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a></h3>
<code><a href="../../mmj/lang/Hyp.html#active">active</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.Stmt">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></h3>
<code><a href="../../mmj/lang/Stmt.html#DESC_NBR_PROOF_REFS">DESC_NBR_PROOF_REFS</a>, <a href="../../mmj/lang/Stmt.html#exprParseTree">exprParseTree</a>, <a href="../../mmj/lang/Stmt.html#LABEL">LABEL</a>, <a href="../../mmj/lang/Stmt.html#logHypsL1HiLoKey">logHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#logHypsMaxDepth">logHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#nbrProofRefs">nbrProofRefs</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="fields_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Fields inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#chapterNbr">chapterNbr</a>, <a href="../../mmj/lang/MObj.html#description">description</a>, <a href="../../mmj/lang/MObj.html#isTempObject">isTempObject</a>, <a href="../../mmj/lang/MObj.html#SECTION_AND_MOBJ_NBR">SECTION_AND_MOBJ_NBR</a>, <a href="../../mmj/lang/MObj.html#sectionMObjNbr">sectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#sectionNbr">sectionNbr</a>, <a href="../../mmj/lang/MObj.html#seq">seq</a>, <a href="../../mmj/lang/MObj.html#SEQ">SEQ</a></code></li>
</ul>
</li>
</ul>
<!-- ======== CONSTRUCTOR SUMMARY ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_summary">
<!--   -->
</a>
<h3>Constructor Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Constructor Summary table, listing constructors, and an explanation">
<caption><span>Constructors</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier</th>
<th class="colLast" scope="col">Constructor and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>&nbsp;</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#VarHyp(int, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.lang.String)">VarHyp</a></strong>(int&nbsp;seq,
      java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
      java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
      java.lang.String&nbsp;varS,
      java.lang.String&nbsp;labelS,
      java.lang.String&nbsp;typS)</code>
<div class="block">Construct VarHyp using sequence number plus label, Type Code and Var
 Strings.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>protected </code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#VarHyp(int, java.lang.String, mmj.lang.Formula)">VarHyp</a></strong>(int&nbsp;tempVarHypSeq,
      java.lang.String&nbsp;tempVarHypLabel,
      <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;tempVarHypFormula)</code>
<div class="block">Construct VarHyp using precomputed values and doing no validation.</div>
</td>
</tr>
</table>
</li>
</ul>
<!-- ========== METHOD SUMMARY =========== -->
<ul class="blockList">
<li class="blockList"><a name="method_summary">
<!--   -->
</a>
<h3>Method Summary</h3>
<table class="overviewSummary" border="0" cellpadding="3" cellspacing="0" summary="Method Summary table, listing methods, and an explanation">
<caption><span>Methods</span><span class="tabEnd">&nbsp;</span></caption>
<tr>
<th class="colFirst" scope="col">Modifier and Type</th>
<th class="colLast" scope="col">Method and Description</th>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#accumVarHypListBySeq(java.util.List)">accumVarHypListBySeq</a></strong>(java.util.List&lt;? super <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;optionalVarHypList)</code>
<div class="block">Accumulate VarHyp(no duplicates), storing it in an array list in order of
 appearance in the database.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>boolean</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#containedInVarHypListBySeq(java.util.List)">containedInVarHypListBySeq</a></strong>(java.util.List&lt;? super <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;mandHypList)</code>
<div class="block">Searches for this Var Hyp in an ArrayList maintained in database input
 sequence.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#getMandHypArrayLength()">getMandHypArrayLength</a></strong>()</code>
<div class="block">Return the mandatory Hyp array length for this VarHyp.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code><a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#getMandVarHypArray()">getMandVarHypArray</a></strong>()</code>
<div class="block">Return the mandatory VarHyp array for this VarHyp.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code><a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a></code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#getVar()">getVar</a></strong>()</code>
<div class="block">Gets the Var for this VarHyp.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>int</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">renderParsedSubExpr</a></strong>(java.lang.StringBuilder&nbsp;sb,
                   int&nbsp;maxDepth,
                   int&nbsp;maxLength,
                   <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;child)</code>
<div class="block">Converts a parse sub-tree into a sub-expression which is output into a
 String Buffer.</div>
</td>
</tr>
<tr class="altColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#setActive(boolean)">setActive</a></strong>(boolean&nbsp;active)</code>
<div class="block">Sets VarHyp "active", either true or false.</div>
</td>
</tr>
<tr class="rowColor">
<td class="colFirst"><code>void</code></td>
<td class="colLast"><code><strong><a href="../../mmj/lang/VarHyp.html#setVar(mmj.lang.Var)">setVar</a></strong>(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;var)</code>
<div class="block">Sets the Var for this VarHyp.</div>
</td>
</tr>
</table>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.Hyp">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a></h3>
<code><a href="../../mmj/lang/Hyp.html#isActive()">isActive</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.Stmt">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></h3>
<code><a href="../../mmj/lang/Stmt.html#equals(java.lang.Object)">equals</a>, <a href="../../mmj/lang/Stmt.html#getExprParseTree()">getExprParseTree</a>, <a href="../../mmj/lang/Stmt.html#getExprRPN()">getExprRPN</a>, <a href="../../mmj/lang/Stmt.html#getFormula()">getFormula</a>, <a href="../../mmj/lang/Stmt.html#getLabel()">getLabel</a>, <a href="../../mmj/lang/Stmt.html#getNbrProofRefs()">getNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#getTyp()">getTyp</a>, <a href="../../mmj/lang/Stmt.html#hashCode()">hashCode</a>, <a href="../../mmj/lang/Stmt.html#incrementNbrProofRefs()">incrementNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#initNbrProofRefs()">initNbrProofRefs</a>, <a href="../../mmj/lang/Stmt.html#resetLogHypsL1HiLoKey()">resetLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#resetLogHypsMaxDepth()">resetLogHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#setExprParseTree(mmj.lang.ParseTree)">setExprParseTree</a>, <a href="../../mmj/lang/Stmt.html#setExprRPN(mmj.lang.ParseTree.RPNStep[])">setExprRPN</a>, <a href="../../mmj/lang/Stmt.html#setLogHypsL1HiLoKey(java.lang.String)">setLogHypsL1HiLoKey</a>, <a href="../../mmj/lang/Stmt.html#setLogHypsMaxDepth(int)">setLogHypsMaxDepth</a>, <a href="../../mmj/lang/Stmt.html#setTyp(mmj.lang.Cnst)">setTyp</a>, <a href="../../mmj/lang/Stmt.html#toString()">toString</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_mmj.lang.MObj">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;mmj.lang.<a href="../../mmj/lang/MObj.html" title="class in mmj.lang">MObj</a></h3>
<code><a href="../../mmj/lang/MObj.html#getChapterNbr()">getChapterNbr</a>, <a href="../../mmj/lang/MObj.html#getDescription()">getDescription</a>, <a href="../../mmj/lang/MObj.html#getDescriptionForSearch()">getDescriptionForSearch</a>, <a href="../../mmj/lang/MObj.html#getIsTempObject()">getIsTempObject</a>, <a href="../../mmj/lang/MObj.html#getOrigSectionNbr()">getOrigSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionMObjNbr()">getSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#getSectionNbr()">getSectionNbr</a>, <a href="../../mmj/lang/MObj.html#getSeq()">getSeq</a>, <a href="../../mmj/lang/MObj.html#setChapterNbr(int)">setChapterNbr</a>, <a href="../../mmj/lang/MObj.html#setDescription(java.lang.String)">setDescription</a>, <a href="../../mmj/lang/MObj.html#setIsTempObject(boolean)">setIsTempObject</a>, <a href="../../mmj/lang/MObj.html#setSectionMObjNbr(int)">setSectionMObjNbr</a>, <a href="../../mmj/lang/MObj.html#setSectionNbr(int)">setSectionNbr</a></code></li>
</ul>
<ul class="blockList">
<li class="blockList"><a name="methods_inherited_from_class_java.lang.Object">
<!--   -->
</a>
<h3>Methods inherited from class&nbsp;java.lang.Object</h3>
<code>clone, finalize, getClass, notify, notifyAll, wait, wait, wait</code></li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
<div class="details">
<ul class="blockList">
<li class="blockList">
<!-- ============ FIELD DETAIL =========== -->
<ul class="blockList">
<li class="blockList"><a name="field_detail">
<!--   -->
</a>
<h3>Field Detail</h3>
<a name="paSubst">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>paSubst</h4>
<pre>public&nbsp;<a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a> paSubst</pre>
<div class="block">paSubst is used in Proof Assistant unification and holds the root node of
 a subtree which is the assigned substitution value for the VarHyp in a
 single ProofStep.
 <p>
 Yes, this is a hokey scratchpad. In theory an array of paSubst could be
 devised, with one entry for each thread :-) Or not.</div>
</li>
</ul>
</li>
</ul>
<!-- ========= CONSTRUCTOR DETAIL ======== -->
<ul class="blockList">
<li class="blockList"><a name="constructor_detail">
<!--   -->
</a>
<h3>Constructor Detail</h3>
<a name="VarHyp(int, java.util.Map, java.util.Map, java.lang.String, java.lang.String, java.lang.String)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>VarHyp</h4>
<pre>public&nbsp;VarHyp(int&nbsp;seq,
      java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Sym.html" title="class in mmj.lang">Sym</a>&gt;&nbsp;symTbl,
      java.util.Map&lt;java.lang.String,<a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a>&gt;&nbsp;stmtTbl,
      java.lang.String&nbsp;varS,
      java.lang.String&nbsp;labelS,
      java.lang.String&nbsp;typS)
       throws <a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></pre>
<div class="block">Construct VarHyp using sequence number plus label, Type Code and Var
 Strings.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>seq</code> - MObj.seq number</dd><dd><code>symTbl</code> - Symbol Table (Map)</dd><dd><code>stmtTbl</code> - Statement Table (Map)</dd><dd><code>varS</code> - Var id String.</dd><dd><code>labelS</code> - Statement label String.</dd><dd><code>typS</code> - Type Code id String.</dd>
<dt><span class="strong">Throws:</span></dt>
<dd><code><a href="../../mmj/lang/LangException.html" title="class in mmj.lang">LangException</a></code> - if duplicate, etc.</dd></dl>
</li>
</ul>
<a name="VarHyp(int, java.lang.String, mmj.lang.Formula)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>VarHyp</h4>
<pre>protected&nbsp;VarHyp(int&nbsp;tempVarHypSeq,
      java.lang.String&nbsp;tempVarHypLabel,
      <a href="../../mmj/lang/Formula.html" title="class in mmj.lang">Formula</a>&nbsp;tempVarHypFormula)</pre>
<div class="block">Construct VarHyp using precomputed values and doing no validation.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>tempVarHypSeq</code> - MObj.seq</dd><dd><code>tempVarHypLabel</code> - Stmt.label</dd><dd><code>tempVarHypFormula</code> - Stmt.formula</dd></dl>
</li>
</ul>
</li>
</ul>
<!-- ============ METHOD DETAIL ========== -->
<ul class="blockList">
<li class="blockList"><a name="method_detail">
<!--   -->
</a>
<h3>Method Detail</h3>
<a name="setActive(boolean)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setActive</h4>
<pre>public&nbsp;void&nbsp;setActive(boolean&nbsp;active)</pre>
<div class="block">Sets VarHyp "active", either true or false.
 <p>
 Sets "active" to true or false. Also, if the new setting is "inactive",
 then the associated var.activeVarHyp is set to null (which happens at the
 end of a scope definition -- see LogicalSystem.)</div>
<dl>
<dt><strong>Overrides:</strong></dt>
<dd><code><a href="../../mmj/lang/Hyp.html#setActive(boolean)">setActive</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Hyp.html" title="class in mmj.lang">Hyp</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>active</code> - true or false.</dd></dl>
</li>
</ul>
<a name="getVar()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getVar</h4>
<pre>public&nbsp;<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;getVar()</pre>
<div class="block">Gets the Var for this VarHyp.
 <p>
 "De-embeds" the var from the VarHyp's VarHypFormula.
 <p>
 A "var" occurrence was stored redundantly here in VarHyp at one time, but
 it was not much used and was later eliminated as being "a waste of code".</div>
<dl><dt><span class="strong">Returns:</span></dt><dd>Var for this VarHyp.</dd></dl>
</li>
</ul>
<a name="setVar(mmj.lang.Var)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>setVar</h4>
<pre>public&nbsp;void&nbsp;setVar(<a href="../../mmj/lang/Var.html" title="class in mmj.lang">Var</a>&nbsp;var)</pre>
<div class="block">Sets the Var for this VarHyp.
 <p>
 A "var" occurrence was stored redundantly here in VarHyp at one time, but
 it was not much used and was later eliminated as being "a waste of code".</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>var</code> - the new Var for the VarHypFormula.</dd></dl>
</li>
</ul>
<a name="getMandVarHypArray()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandVarHypArray</h4>
<pre>public&nbsp;<a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>[]&nbsp;getMandVarHypArray()</pre>
<div class="block">Return the mandatory VarHyp array for this VarHyp.
 <p>
 I'd rather not explain this one, but at the time I coded it, I must have
 been thinking something... It appears useless, but ...</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#getMandVarHypArray()">getMandVarHypArray</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>Mandatory VarHyp Array for this VarHyp.</dd></dl>
</li>
</ul>
<a name="getMandHypArrayLength()">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>getMandHypArrayLength</h4>
<pre>public&nbsp;int&nbsp;getMandHypArrayLength()</pre>
<div class="block">Return the mandatory Hyp array length for this VarHyp.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#getMandHypArrayLength()">getMandHypArrayLength</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Returns:</span></dt><dd>Mandatory VarHyp Array Length for this VarHyp.</dd></dl>
</li>
</ul>
<a name="renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>renderParsedSubExpr</h4>
<pre>public&nbsp;int&nbsp;renderParsedSubExpr(java.lang.StringBuilder&nbsp;sb,
                      int&nbsp;maxDepth,
                      int&nbsp;maxLength,
                      <a href="../../mmj/lang/ParseNode.html" title="class in mmj.lang">ParseNode</a>[]&nbsp;child)</pre>
<div class="block">Converts a parse sub-tree into a sub-expression which is output into a
 String Buffer.
 <p>
 Note: this will not work for a proof node! The ParseNode's stmt must be a
 VarHyp or a Syntax Axiom.
 <p>
 The output sub-expression is generated into text not to exceed the given
 maxLength. If the number of output characters exceeds maxLength output
 terminates, possibly leaving a dirty StringBuilder.
 <p>
 The depth of the sub-tree is checked against the input maxDepth
 parameter, and if the depth exceeds this number, output terminates,,
 possibly leaving a dirty StringBuilder.
 <p>
 Depth is computed as 1 for each Notation Syntax Axiom Node. VarHyp nodes
 and Nulls Permitted, Type Conversion and NamedTypedConstant Syntax Axiom
 nodes are assigned depth = 0 for purposes of depth checking.</div>
<dl>
<dt><strong>Specified by:</strong></dt>
<dd><code><a href="../../mmj/lang/Stmt.html#renderParsedSubExpr(java.lang.StringBuilder, int, int, mmj.lang.ParseNode[])">renderParsedSubExpr</a></code>&nbsp;in class&nbsp;<code><a href="../../mmj/lang/Stmt.html" title="class in mmj.lang">Stmt</a></code></dd>
<dt><span class="strong">Parameters:</span></dt><dd><code>sb</code> - StringBuilder already initialized for appending characters.</dd><dd><code>maxDepth</code> - maximum depth of Notation Syntax axioms in sub-tree to be
            printed. Set to Integer.MAX_VALUE to turn off depth checking.</dd><dd><code>maxLength</code> - maximum length of output sub-expression. Set to
            Integer.MAX_VALUE to turn off depth checking.</dd><dd><code>child</code> - array of ParseNode, corresponding to VarHyp nodes to be
            substituted into the Stmt.</dd>
<dt><span class="strong">Returns:</span></dt><dd>length of sub-expression characters appended to the input
         StringBuilder -- or -1 if maxDepth or maxLength exceeded.</dd></dl>
</li>
</ul>
<a name="accumVarHypListBySeq(java.util.List)">
<!--   -->
</a>
<ul class="blockList">
<li class="blockList">
<h4>accumVarHypListBySeq</h4>
<pre>public&nbsp;void&nbsp;accumVarHypListBySeq(java.util.List&lt;? super <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;optionalVarHypList)</pre>
<div class="block">Accumulate VarHyp(no duplicates), storing it in an array list in order of
 appearance in the database.
 <p>
 Because varHypList is maintained in database statement sequence order,
 varHypList should either be empty (new) before the call, or already be in
 that order.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>optionalVarHypList</code> - List of Var Hyps, updated here.</dd></dl>
</li>
</ul>
<a name="containedInVarHypListBySeq(java.util.List)">
<!--   -->
</a>
<ul class="blockListLast">
<li class="blockList">
<h4>containedInVarHypListBySeq</h4>
<pre>public&nbsp;boolean&nbsp;containedInVarHypListBySeq(java.util.List&lt;? super <a href="../../mmj/lang/VarHyp.html" title="class in mmj.lang">VarHyp</a>&gt;&nbsp;mandHypList)</pre>
<div class="block">Searches for this Var Hyp in an ArrayList maintained in database input
 sequence.</div>
<dl><dt><span class="strong">Parameters:</span></dt><dd><code>mandHypList</code> - List of Var Hyps</dd>
<dt><span class="strong">Returns:</span></dt><dd>true if found, else false.</dd></dl>
</li>
</ul>
</li>
</ul>
</li>
</ul>
</div>
</div>
<!-- ========= END OF CLASS DATA ========= -->
<!-- ======= START OF BOTTOM NAVBAR ====== -->
<div class="bottomNav"><a name="navbar_bottom">
<!--   -->
</a><a href="#skip-navbar_bottom" title="Skip navigation links"></a><a name="navbar_bottom_firstrow">
<!--   -->
</a>
<ul class="navList" title="Navigation">
<li><a href="../../overview-summary.html">Overview</a></li>
<li><a href="package-summary.html">Package</a></li>
<li class="navBarCell1Rev">Class</li>
<li><a href="package-tree.html">Tree</a></li>
<li><a href="../../deprecated-list.html">Deprecated</a></li>
<li><a href="../../index-all.html">Index</a></li>
<li><a href="../../help-doc.html">Help</a></li>
</ul>
</div>
<div class="subNav">
<ul class="navList">
<li><a href="../../mmj/lang/Var.html" title="class in mmj.lang"><span class="strong">Prev Class</span></a></li>
<li><a href="../../mmj/lang/VarHypFormula.html" title="class in mmj.lang"><span class="strong">Next Class</span></a></li>
</ul>
<ul class="navList">
<li><a href="../../index.html?mmj/lang/VarHyp.html" target="_top">Frames</a></li>
<li><a href="VarHyp.html" target="_top">No Frames</a></li>
</ul>
<ul class="navList" id="allclasses_navbar_bottom">
<li><a href="../../allclasses-noframe.html">All Classes</a></li>
</ul>
<div>
<script type="text/javascript"><!--
  allClassesLink = document.getElementById("allclasses_navbar_bottom");
  if(window==top) {
    allClassesLink.style.display = "block";
  }
  else {
    allClassesLink.style.display = "none";
  }
  //-->
</script>
</div>
<div>
<ul class="subNavList">
<li>Summary:&nbsp;</li>
<li>Nested&nbsp;|&nbsp;</li>
<li><a href="#field_summary">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_summary">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_summary">Method</a></li>
</ul>
<ul class="subNavList">
<li>Detail:&nbsp;</li>
<li><a href="#field_detail">Field</a>&nbsp;|&nbsp;</li>
<li><a href="#constructor_detail">Constr</a>&nbsp;|&nbsp;</li>
<li><a href="#method_detail">Method</a></li>
</ul>
</div>
<a name="skip-navbar_bottom">
<!--   -->
</a></div>
<!-- ======== END OF BOTTOM NAVBAR ======= -->
</body>
</html>
